//package kodkod.analysis;
//
//import java.util.*;
//
//import kodkod.analysis.AST.Analyzer;
//import kodkod.ast.*;
//import kodkod.ast.operator.ExprOperator;
//import kodkod.instance.Tuple;
//import kodkod.instance.TupleSet;
//
//public class Dominance {
//	
//	Expression exp;
//	
//	HashMap<Expression, Double> positive = new HashMap<Expression, Double>();
//	HashMap<Expression, Double> negative = new HashMap<Expression, Double>();
//	
//	public Dominance(Expression e) {
//		this.exp = e;
//		
//		if (e instanceof UnaryExpression)			init((UnaryExpression)e);
//		else if (e instanceof BinaryExpression)		init((BinaryExpression)e);
//		else if (e instanceof NaryExpression)		init((NaryExpression)e);
//		else if (e instanceof Comprehension)		init((Comprehension)e);
//		else if (e instanceof IfExpression)			init((IfExpression)e);
//		else if (e instanceof ProjectExpression)	init((ProjectExpression)e);
//		else if (e instanceof IntToExprCast) 		init((IntToExprCast)e);
//	}
//	
//	public double getPositiveDominance(LeafExpression leaf) {
//		if (exp == leaf) return 1;
//		
//		double dominance = 0;
//		
//		for (Expression child : positive.keySet()) {
//			Dominance recursion = new Dominance(child);
//			dominance += positive.get(child) * recursion.getPositiveDominance(leaf);
//		}
//		
//		return Double.isNaN(dominance) ? 0 : dominance;
//	}
//	
//	public double getNegativeDominance(LeafExpression leaf) {
//		if (exp == leaf) return 1;
//		
//		double dominance = 0;
//		
//		for (Expression child : negative.keySet()) {
//			Dominance recursion = new Dominance(child);
//			dominance += negative.get(child) * recursion.getNegativeDominance(leaf);
//		}
//		
//		return Double.isNaN(dominance) ? 0 : dominance;
//	}
//	
//	public void init(UnaryExpression e) {
//		positive.put(e.expression(), 1.0);
//		negative.put(e.expression(), 1.0);
//	}
//	
//	public void init(BinaryExpression e) {
//		BoundsExtension bounds1 = BoundsExtension.get(e.left());
//		BoundsExtension bounds2 = BoundsExtension.get(e.right());
//		
//		double numerator, denominator;
//		
//		switch (e.op()) {
//		case UNION:
//		case INTERSECTION:
//		case PRODUCT:
//		case OVERRIDE:
//			// use the general implementation for n-ary expressions
//			ArrayList<Expression> list = new ArrayList<Expression>();
//			list.add(e.left());
//			list.add(e.right());
//			
//			for (Expression child : list) {
//				denominator = getDenominator(child);
//				
//				numerator = getNumerator(child, list, e.op(), true);
//				positive.put(child, numerator / denominator);
//				
////				System.out.println(child + " in " + exp);
////				System.out.println("+numerator " + numerator);
////				System.out.println("denominator " + denominator);
//				
//				numerator = getNumerator(child, list, e.op(), false);
//				negative.put(child, numerator / denominator);
//				
////				System.out.println(child + " in " + exp);
////				System.out.println("-numerator " + numerator);
////				System.out.println("denominator " + denominator);
//			}
//			break;
//		case DIFFERENCE:
//			denominator = getDenominator(e.left());
//			
//			numerator = intersection(bounds1.free, bounds2.upper).size() + (double)intersection(bounds1.free, bounds2.free).size() / 2.0;
//			positive.put(e.left(), numerator / denominator);
//			numerator = intersection(bounds1.free, bounds2.lower).size();
//			negative.put(e.left(), numerator / denominator);
//			
//			denominator = getDenominator(e.right());
//			
//			numerator = intersection(bounds2.free, bounds1.upper).size() + (double)intersection(bounds2.free, bounds1.free).size() / 2.0;
//			positive.put(e.right(), numerator / denominator);
//			numerator = intersection(bounds2.free, bounds1.lower).size();
//			negative.put(e.right(), numerator / denominator);
//			
//			break;
//		
//		case JOIN:
//			double nofConst, nofOpen;
//			
//			nofConst = 0.0;
//			nofOpen = 0.0;
//			denominator = getDenominator(e.left());
//			
//			for (Tuple tuple : bounds1.free) {
//				Object connector1 = tuple.atom(tuple.arity()-1);
//				for (Tuple tuple2 : bounds2.lower) {
//					Object connector2 = tuple2.atom(0);
//					if (connector1 == connector2) nofConst++;
//				}
//				for (Tuple tuple2 : bounds2.free) {
//					Object connector2 = tuple2.atom(0);
//					if (connector1 == connector2) nofOpen++;
//				}
//			}
//			
//			numerator = nofConst + nofOpen / 2;
//			positive.put(e.left(), numerator / denominator);
//			
//			nofConst = 0.0;
//			nofOpen = 0.0;
//			denominator = getDenominator(e.right());
//			
//			for (Tuple tuple : bounds2.free) {
//				Object connector1 = tuple.atom(0);
//				for (Tuple tuple2 : bounds1.lower) {
//					Object connector2 = tuple2.atom(tuple2.arity()-1);
//					if (connector2 == connector1) nofConst++;
//				}
//				for (Tuple tuple2 : bounds1.free) {
//					Object connector2 = tuple2.atom(tuple2.arity()-1);
//					if (connector2 == connector1) nofOpen++;
//				}
//			}
//			numerator = nofConst + nofOpen / 2;
//			positive.put(e.right(), numerator / denominator);
//			
//			numerator = 0;
//			denominator = getDenominator(e.left());
//			
//			for (Tuple tuple : bounds1.free) {
//				Object connector1 = tuple.atom(tuple.arity()-1);
//				nofConst = 0;
//				for (Tuple tuple2 : bounds2.lower) {
//					Object connector2 = tuple2.atom(0);
//					if (connector1 == connector2) nofConst++;
//				}
//				nofOpen = 0;
//				for (Tuple tuple2 : bounds2.free) {
//					Object connector2 = tuple2.atom(0);
//					if (connector1 == connector2) nofOpen++;
//				}
//				numerator += nofConst + nofOpen / (nofOpen + nofConst);
//			}
//			negative.put(e.left(), numerator / denominator);
//			
//			numerator = 0;
//			denominator = getDenominator(e.right());
//			
//			for (Tuple tuple : bounds2.free) {
//				Object connector1 = tuple.atom(0);
//				nofConst = 0;
//				for (Tuple tuple2 : bounds1.lower) {
//					Object connector2 = tuple2.atom(tuple2.arity()-1);
//					if (connector2 == connector1) nofConst++;
//				}
//				nofOpen = 0;
//				for (Tuple tuple2 : bounds1.free) {
//					Object connector2 = tuple2.atom(tuple2.arity()-1);
//					if (connector1 == connector2) nofOpen++;
//				}
//				numerator += nofConst + nofOpen / (nofOpen + nofConst);
//			}
//			negative.put(e.right(), numerator / denominator);
//			
//			break;
//		default: break;
//		}
//	}
//	
//	public void init(NaryExpression e) {
//		double numerator, denominator;
//		
//		ArrayList<Expression> list = new ArrayList<Expression>();
//		for (Expression child : e) list.add(child);
//		
//		for (Expression child : list) {
//			denominator = getDenominator(child);
//			
//			numerator = getNumerator(child, list, e.op(), true);
//			positive.put(child, numerator / denominator);
//			numerator = getNumerator(child, list, e.op(), false);
//			negative.put(child, numerator / denominator);
//		}
//	}
//	
//	public void init(Comprehension e) {
//		double numerator, denominator;
//		
//		ArrayList<Expression> list = new ArrayList<Expression>();
//		for (Decl decl : e.decls()) list.add(decl.expression());
//		
//		if (list.size() == 1) {
//			positive.put(list.get(0), 1.0);
//			negative.put(list.get(0), 1.0);
//			return;
//		}
//		
//		for (Expression child : list) {
//			denominator = getDenominator(child);
//			
//			numerator = getNumerator(child, list, ExprOperator.PRODUCT, true);
//			positive.put(child, numerator / denominator);
//			numerator = getNumerator(child, list, ExprOperator.PRODUCT, false);
//			negative.put(child, numerator / denominator);
//		}
//	}
//	
//	public void init(IfExpression e) {
//		positive.put(e.thenExpr(), 1.0);
//		positive.put(e.elseExpr(), 1.0);
//		negative.put(e.thenExpr(), 1.0);
//		negative.put(e.elseExpr(), 1.0);
//	}
//	
//	public void init(ProjectExpression e) {
//		positive.put(e.expression(), 1.0);
//		negative.put(e.expression(), 1.0);
//	}
//	
//	public void init(IntToExprCast e) {
////		positive.put(e.intExpr(), 1.0);
////		negative.put(e.intExpr(), 1.0);
//	}
//	
//	private double getNumerator(Expression child, ArrayList<Expression> gate, ExprOperator type, boolean positive) {
//		assert(gate.contains(child));
//		assert(gate.size() > 1);
//		
//		double numerator = 0.0;
//		
//		BoundsExtension childBounds = BoundsExtension.get(child);
//		
//		// although "gate" contains "child", "gateBounds" will _not_ contain "childBounds"
//		ArrayList<BoundsExtension> gateBounds = new ArrayList<BoundsExtension>();
//		for (Expression e : gate) if (e != child) gateBounds.add(BoundsExtension.get(e));
//		
//		while (gateBounds.size() < gate.size() - 1) gateBounds.add(BoundsExtension.get(child)); //bugfix (self-product,..)
//		
//		ArrayList<TupleSet> upperBounds = new ArrayList<TupleSet>();
//		ArrayList<TupleSet> lowerBounds = new ArrayList<TupleSet>();
//		ArrayList<TupleSet> freeBounds = new ArrayList<TupleSet>();
//		for (BoundsExtension b : gateBounds) upperBounds.add(b.upper);
//		for (BoundsExtension b : gateBounds) lowerBounds.add(b.lower);
//		for (BoundsExtension b : gateBounds) freeBounds.add(b.free);
//		
//		switch (type) {
//		case UNION:
//			if (positive) {
//				numerator = difference(childBounds.free, union(lowerBounds)).size();
//			} else {
//				numerator = difference(childBounds.free, union(upperBounds)).size();
//				numerator += (double)intersection(childBounds.free, union(freeBounds)).size() / (1.0+intersection(freeBounds).size()); // abbreviation: max(gatesize)
//			}
//			break;
//		case INTERSECTION:
//			if (positive) {
//				numerator = difference(childBounds.free, union(lowerBounds)).size();
//				numerator += (double)intersection(childBounds.free, union(freeBounds)).size() / (1.0+intersection(freeBounds).size()); // abbreviation: max(gatesize)
//			} else {
//				numerator = difference(childBounds.free, union(upperBounds)).size();
//			}
//			break;
//		case PRODUCT:
//			if (positive) {
//				numerator = childBounds.free.size() * union(lowerBounds).size();
//				numerator += (double)(childBounds.free.size() * union(freeBounds).size()) / (1.0+intersection(freeBounds).size()); // abbreviation: max(gatesize)
//			} else {
//				numerator = childBounds.free.size() * union(upperBounds).size();
//			}
//			break;
//		case OVERRIDE:
//			double index = gate.indexOf(child);
//			numerator = index / (double)gateBounds.size(); 
//			
////			if (positive) {
////				numerator = 0;
////				for (Tuple t : childBounds.free) {
////					boolean overridden = false;
////					for (Tuple t2 : union(lowerBounds)) {
////						if (t.atom(0) == t2.atom(0)) overridden = true;
////					}
////					if (overridden) continue;
////					double gatesize = 1;
////					for (BoundsExtension b : gateBounds) {
////						for (Tuple t2 : b.free) {
////							if (t.atom(0) == t2.atom(0)) gatesize++;
////						}
////					}
////					numerator += 1.0 / gatesize;
////				}
////				
////				numerator = 1;
////			} else {
////				numerator = 1;
////			}
//			break;
//		}
//		
//		return numerator;
//	}
//	
//	private double getDenominator(Expression e) {
//		double denominator = 1;
//		
//		BoundsExtension bounds = BoundsExtension.get(e);
//		denominator *= bounds.free.size();
//		
//		return denominator == 0 ? 1 : denominator;
//	}
//	
//	private TupleSet intersection(ArrayList<TupleSet> list) {
//		try {
//			TupleSet result = list.get(0).clone();
//			for (TupleSet elem : list) {
//				result.retainAll(elem);
//			}
//			return result;
//		} catch (IndexOutOfBoundsException e) {
//			e.printStackTrace();
//			System.exit(-1);
//			return null;
//		}
//	}
//	
//	private TupleSet union(ArrayList<TupleSet> list) {
//		try {
//			TupleSet result = list.get(0).clone();
//			for (TupleSet elem : list) {
//				result.addAll(elem);
//			}
//			return result;
//		} catch (IndexOutOfBoundsException e) {
//			e.printStackTrace();
//			System.exit(-1);
//			return null;
//		}
//	}
//	
//	public static TupleSet intersection(TupleSet c1, TupleSet c2) {
//		TupleSet result = c1.clone();
//		result.retainAll(c2);
//		return result;
//	}
//	
//	public static TupleSet union(TupleSet c1, TupleSet c2) {
//		TupleSet result = c1.clone();
//		result.addAll(c2);
//		return result;
//	}
//	
//	public static TupleSet difference(TupleSet c1, TupleSet c2) {
//		TupleSet result = c1.clone();
//		result.removeAll(c2);
//		return result;
//	}
//}
